#!/bin/sh
#
# compares with lesar the semantics  of 2 lustre programs
# using lesar and lurette.


EXPECTED_ARGS=4

if [ $# -ne $EXPECTED_ARGS ]
then
    echo "usage: $0 lustrefile1 node1 lustrefile2 node2

    Launch Lurette to check if node1 and node2 are not equivalent.
    Launch Lesar to check if node1 and node2 are equivalent.
    "      
else
    file1=$1
    node1=$2
    file2=$3
    node2=$4
    oracle_node=${node1}_oracle
    oracle_file=_${oracle_node}.lus
    riffile=${node1}"_equal_"${node2}.rif
    env=_${node1}_env.lut
    oracle_ec=${node1}_oracle_prog.ec
    
    echo " Are nodes $node1@$file1 and $node2@$file2 different?"
    echo " let's check it with lurette... "
    # set -x #echo on
    
    if
        lus2lic $file1 -n $node1 --gen-autotest -np;
        then
        echo "lus2lic --gen-autotest done"
    else
        echo "Error when calling 'lus2lic $file1 -n $node1 --gen-autotest -np'"
        exit 2
    fi
    
    . /home/jahier/.opam/opam-init/variables.sh

    lus2lic $file1 -n $node1 -ec  >> $oracle_file ;
    lus2lic $file2 -n $node2 -ec  >> $oracle_file ;
    echo "node P1 = ${node1}"  >> $oracle_file;
    echo "node P2 = ${node2}"  >> $oracle_file;

    lurette -l 100 -o $ {riffile} \
        -sut "lus2lic $file2 -n $node2" \
        -env "lutin -seed 42 $env" \
        -oracle "lus2lic $oracle_file -n $oracle_node"

    set - #echo off
    if [ $? -eq 0 ] # Test du code de sortie de la commande "lurette".
        then
        echo " ===> nodes $node1@$file1 and $node2@$file2 _SEEMS_ to be equivalent"
        echo " let's check it with lesar... "
    else if [ $? -eq 1 ] 
        then
        echo " ===> nodes $node1@$file1 and $node2@$file2 _ARE NOT_ equivalent (cf ${riffile}"
        exit 
    else
        echo " A pb occured in lurettop (exit $?)"
        exit 
    fi
    fi
    set -x #echo on
    lus2lic -ec ${oracle_file} -n ${node1}_oracle_prog -o ${oracle_ec}
    ecverif ${oracle_ec}

    set - #echo off
    if [ $? -eq 0 ] # Test du code de sortie de la commande "lurette".
        then
        echo
        echo  " ===> nodes $node1@$file1 and $node2@$file2 _ARE_ equivalent"
    else
        echo " ===> nodes $node1@$file1 and $node2@$file2 _seems_ to differ"
    fi

    echo "rm ${env} ${oracle_file} ${riffile} ${oracle_ec}" > lustrequiv-clean-me
    echo "rm  *.cm* *.o luretteSession* *.log  " >> lustrequiv-clean-me
    echo "rm lurette.cov my-rdbg-tuning.ml lustrequiv-clean-me" >> lustrequiv-clean-me
    echo "To clean up this mess, consider doing a \n\t sh lustrequiv-clean-me"
    exit 0
fi